\documentclass[11pt]{article}
\usepackage{k2latex.bb}
\usepackage[noline,boxruled]{algorithm2e}


\hoffset=-1cm
\textwidth=14cm
\marginparwidth=25pt
\topmargin=-2cm
%\footskip=4cm
\textheight=22cm

\begin{document}

% title
\title{Contextual transformations\\in K Framework}%
\author{Andrei Arusoaie and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a}\\Faculty of Computer Science, Alexandru Ioan Cuza University, Romania\\\texttt{\{andrei.arusoaie,traian.serbanuta\}$@$info.uaic.ro}}%
%\today
%\maketitle%


A \K definition for a programming language is compiled into a rewrite theory by applying some transformations steps. One of them is the contextual transformation. To improve the modularity of definitions, a \K rule only specifies the {\em minimal required} context for its application. The contextual transformation step uses static information about the structure of the global running configuration to infer {\em sufficiently}  additional context to make the rule match and apply on the running configuration. Figure \ref{ct:lookup-transformed} describes the effect of contextual transformation applied on the variable lookup rule (left) according to SIMPLE~\cite{ct:kpage} configuration.

Although the K-Maude prototype already provides an implementation for context transformations, this implementations lacks certain features which are important for the development of complex definitions, such as the \K definition for the C language~\cite{csem}. Some limitations of the existing approach are that (1) the configuration cannot contain cells with the same name, (2) the cases where the context transformations could have more than one solution are not analyzed, and (3) the {\em locality principle} does not have yet an unanimously agreed formal specification. An investigation of all these limitations is required in order to obtain a correct contextual transformation algorithm. 

\begin{figure}
\centering
\begin{tabular}{|l|r|}
\hline
\hspace{-10ex}\begin{minipage}{.5\textwidth}
\vspace{2ex}
\fontsize{5}{5}\selectfont
\kallLarge{white}{T}{\hspace{-15ex}\kallLarge{white}{threads}{\hspace{-10ex}\kallLarge{white}{thread *}{\kallLarge{white}{k}{\variable{K}{K}}\kallLarge{white}{env}{\dotCt{Map}}\kallLarge{white}{holds}{\dotCt{Map}}\kBR \kallLarge{white}{control}{\kallLarge{white}{fstack}{\dotCt{List}}\kallLarge{white}{xstack}{\dotCt{List}}}\hspace{-3ex}}\hspace{-10ex}}\hspace{-15ex}  \kBR \kallLarge{white}{genv}{\dotCt{Map}}\kallLarge{white}{store}{\dotCt{Map}}\kallLarge{white}{busy}{\dotCt{Set}} \kBR \kallLarge{white}{in}{\dotCt{List}}\kallLarge{white}{out}{\dotCt{List}}\kallLarge{white}{nextLoc}{\constant{0}{Zero}}}
\vspace{5ex}\end{minipage} \hspace{-10ex}
&
\begin{minipage}{.45\textwidth}
\centering
\fontsize{6}{6}\selectfont
{\ensuremath{{{{\kprefix{white}{k}{\reduce{\variable{X}{Id}}{\variable{V}{Val}}}}\mathrel{\terminal{}}{\kmiddle{white}{env}{{{\variable{X}{Id}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{L}{Nat}}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{V}{Val}}}}}}}

{\huge $\downarrow$}

${\ensuremath \kmiddle{white}{T}{{{\kmiddle{white}{threads}{\kmiddle{white}{thread}{{{\kprefix{white}{k}{\reduce{\variable{X}{Id}}{\variable{V}{Val}}}}\mathrel{\terminal{}}{\kmiddle{white}{env}{{{\variable{X}{Id}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{L}{Nat}}}}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{V}{Val}}}}}}}}$
\end{minipage}\\
\hline
\end{tabular}
\caption{SIMPLE: configuration (left), variable lookup rule (top-right) and variable lookup rule context (top-left)}
\label{ct:lookup-transformed}
\end{figure}

Because of contextual transformations, \K has two big advantages: 
\begin{itemize}
\item abstraction, given by the fact that a user specifies in an abstract way the items of interest from configuration without caring about the concrete configuration, and 
\item
 modularity, given by the fact that in an existing definition a user can add more items in the configuration and rules without modifying the existing definition
\end{itemize}

For the next version of K we propose a slight different approach which is intented to treat limitations (1), (2), and (3). The new algorithm searches for all possible matchings of the rule in the configuration. For each matching the {\it minimal context} is computed and then the matching is filtered by a {\it consistency filter} which ensures multiplicity consitency, and a {\it locality filter} which applies the locality principle. If there are more than one possible context after all these checks then an ambiguity error is reported. . A pseudocode for the general contextual transformation algorithm is given by Function \ref{ct:algorithm}. 

\begin{function}
\SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output}
\Input{configuration, rule}
\Output{rule context or ambiguity error}
\Begin{
	Let M be the set of all possible matchings of rule in configuration\;
	M' = $\emptyset$\;
	min = $\infty$\;
	\For {m $\in$ M}
	{
		\uIf {m is consistent}
		{
			Let m' be the minimal context of m\;
			\uIf {min > cellsNo(m')}
			{	
				M' = \{ m' \}\;
				min = cellsNo(m');
			}
			\uIf {min = cellsNo(m')} {M' = M' $\cup$ \{ m' \} \; }
		}
	}
	\eIf {|M| = 1}
	{ \tcp{ assume M = \{ m \}} \Return{m} \;}
	{\Return{"Rule is ambiguous!"} \;} 
}
\caption{context-transformation(configuration, rule)}
\label{ct:algorithm}
\end{function}


\bibliographystyle{plain}
\bibliography{mibib}


\end{document}